package systemfnomabss.syntax

trait Binding { // self: BindingSyntax with Binding => 
  type Name

  trait Nominal[Self] {
    def swap(a: Name, b: Name): Self
    def fresh(a: Name): Boolean
    def supp: List[Name]
  }

  implicit def IntIsNominal(self: Int): Nominal[Int] = new Nominal[Int] {
    def swap(a: Name, b: Name) = self
    def fresh(a: Name) = true
    def supp = List()
  }  

  implicit def CharIsNominal(self: Char): Nominal[Char] = new Nominal[Char] {
    def swap(a: Name, b: Name) = self
    def fresh(a: Name) = true
    def supp = List()
  } 
  
  implicit def UnitIsNominal(self: Unit): Nominal[Unit] = new Nominal[Unit] {
    def swap(a: Name, b: Name) = self
    def fresh(a: Name) = true
    def supp = List()
  }   
  
// can't abstract over Iterable here because it isn't defined like that in std lib
  
  implicit def ListIsNominal[T <% Nominal[T]](self: List[T]): Nominal[List[T]] = new Nominal[List[T]] {
    def swap(a: Name, b: Name) = self map (_.swap(a, b))    
    def fresh(a: Name) = self forall (_.fresh(a))
    def supp = (self flatMap (_.supp)).toList
  }   
  
  implicit def OptionIsNominal[T <% Nominal[T]](self: Option[T]): Nominal[Option[T]] = new Nominal[Option[T]] {
    def swap(a: Name, b: Name) = self map (_.swap(a, b))    
    def fresh(a: Name) = self forall (_.fresh(a))
    def supp = (self.toList flatMap (_.supp)).toList
  }     
  
  implicit def SetIsNominal[T <% Nominal[T]](self: Set[T]): Nominal[Set[T]] = new Nominal[Set[T]] {
    def swap(a: Name, b: Name) = self map (_.swap(a, b))    
    def fresh(a: Name) = self forall (_.fresh(a))
    def supp = (self flatMap (_.supp)).toList
  }     
  
}



trait BindingSyntax { self: Binding  with BindingSyntax => //self: AbsM with Binding with Substitution with BindingSyntax =>
//trait Equality[T] {
//      def ===(a: T): Boolean
//}

type Tag = Int


object Name {
  private[Name] var nextTag: Int = -1 // only for toString
  def apply(name:Name) = new Name(name.name)
  def apply(name:String) = new Name(name)
}
class Name(val name: String) extends Nominal[Name] {
  def \\[T](body: T)(implicit c: T => Nominal[T]): \\[T] = new \\[T](this, body)
  
  override def equals(o: Any): Boolean =  o match {
    case n: Name  => n eq this //if n.tag == t => true
    case _ => false
  }
  
  def swap(a: Name, b: Name) = if(this == a) b else if(this == b) a else this
  def fresh(a: Name) = this != a
  def supp = List(this)    
  val tag:Tag =  {Name.nextTag +=1; Name.nextTag}
  override def toString = name + "$" + tag
}

//def gensym(s: String): AM[Name] = for( t <- AM.newTag) yield Name(t, s)
//def rename(a: Name): AM[Name] = for( t <- AM.newTag) yield Name(t, a.s) //subsumed by name.apply

object \\ {
  def apply[T](binder: Name, body: T)(implicit c: T => Nominal[T]) = new \\[T](binder, body)
  def unapply[T](scrutinee: \\[T])(implicit c: T => Nominal[T]): Option[(Name, T)] = Some(scrutinee unabs)
}

class \\[T](private[BindingSyntax] val binder: Name, private[BindingSyntax] val body: T)(
            implicit val cn: T => Nominal[T]) extends Nominal[\\[T]] {
      
  def unabs: (Name, T) = { val newBinder = Name(binder);  
                             (newBinder, body swap (binder, newBinder)) }
      
  override def equals(o: Any): Boolean = o match {
    case other: \\[T] => (binder == other.binder && body == other.body) ||  // TODO: unchecked!
        (other.body.fresh(binder) && body == other.body.swap(binder, other.binder))
    case _ => false
  }

  
  //def gequals[Eq[x] <: Equality[x] ](other: \\[T])(implicit neq: Name => Eq[Name], beq: T => Eq[T]): Boolean = (binder === other.binder) && (body === other.body) ||  // TODO: unchecked!
  //      (other.body.fresh(binder) && (body === other.body.swap(binder, other.binder)))
  
  def swap(a: Name, b: Name) = \\(binder swap(a, b), body swap(a, b)) // boilerplate
  def fresh(a: Name) = if(a == binder) true else body fresh (a)
  def supp = body.supp filter (_ != binder)        
  
  override def toString = { val (binder,body) = unabs;
                            binder + "\\\\" + body }
  }
      //for(
      //bibo <- unabs;             
      //val (binder, body) = bibo)
      //yield binder + "\\\\" + body).run // NOTE: only useful for local debug output*/
 //}


}

trait Substitution { self: Binding with BindingSyntax with Substitution => // self: AbsM  with Binding with BindingSyntax with Substitution =>
type Name

trait Substable[SubstParam, Self] { 
  //def apply(se:Self):Substable[SubstParam,Self]
  def subst(sub: Name => Option[SubstParam]): Self
  def subst(n: Name, r: SubstParam): Self = subst{case y if n == y => Some(r) case _ => None }
}

class SubstTo[S] {
  type Subst[T] = Substable[S, T]

  implicit def OptionIsSubstable[T <% Subst[T]](self: Option[T]): Subst[Option[T]] = new Substable[S, Option[T]] {
    def subst(sub: Name => Option[S]): Option[T] = self.map(_.subst(sub))
  }

  implicit def SetIsSubstable[T <% Subst[T]](self: Set[T]): Subst[Set[T]] = new Substable[S, Set[T]] {
   def subst(sub: Name => Option[S]): Set[T] = self.map(_.subst(sub))
  }
}

class AbsSubstTo[S] {
  type Subst[T] = Substable[S, T]
  
  implicit def AbsIsSubstable[T](self: \\[T])(implicit c: T => Subst[T]): Subst[\\[T]] = new Substable[S, \\[T]]  {
    implicit val cn: T => Nominal[T] = self.cn
    def subst(sub: Name => Option[S]): \\[T] =  self match {
      case \\(binder, body) => { val body2 = body subst(sub)
                                 binder\\body2 }
      }
      
    //}
    //  for(
    //    bibo <- self.unabs;             // TODO: use unapply pattern to
    //    val (binder, body) =  bibo; // bind (binder, body) directly
    //    body2 <- self.body subst(sub))
    //    yield (binder \\ body2)
  }    
}

}
